;;;
;;; Solution for A3 question #2
;;;
;;; By Philip W. L. Fong
;;;

;;
;; Composition of substitutions
;;

(defun substitution-bound-p (sub sym)
  "Check if symbol SYM is bound in substitution SUB."
  (not (eq sym (substitution-look-up sub sym))))

(defun compose-substitutions (s1 s2)
  "Compose substitution s1 with s2."
  (let ((s3 (mapcar #'(lambda (B) 
			(make-binding (binding-sym B)
				      (apply-substitution s2 (binding-exp B))))
		    s1))
	(s4 (remove-if #'(lambda (B) 
			   (substitution-bound-p s1 (binding-sym B)))
		       s2)))
    (append s3 s4)))

;;
;; Unification
;;

(defun occurs-check-p (var exp)
  "Return non-NIL if variable VAR occurs in expression EXP."
  (cond
   ((null exp) 
    nil)
   ((consp exp)
    (or (occurs-check-p var (first exp))
	(occurs-check-p var (rest exp))))
   (t
    (eq var exp))))

(defun unify (equation-list)
  "Return the substitution that solves the unification equations in the list
EQUATION-LIST, or return 'failure if the list of equations is not solvable."
  (unify-aux nil equation-list))

(defun unify-aux (sub equation-list)
  "Implementation of the Robinson's unification algorithm."
  (if (null equation-list)
      sub
    (let ((t1 (equation-lhs (first equation-list)))
	  (t2 (equation-rhs (first equation-list)))
	  (rest-eqns (rest equation-list)))
      (cond
       ;; Deletion
       ((eq t1 t2)
	(unify-aux sub rest-eqns))
       ;; Binding + Occur-Check
       ((variable-p t1)
	(if (occurs-check-p t1 t2)
	    'failure
	  (unify-aux 
	   (compose-substitutions sub (make-unit-substitution t1 t2))
	   (apply-substitution (make-unit-substitution t1 t2)
			       rest-eqns))))
       ;; Orientation
       ((variable-p t2)
	(unify-aux sub (cons (list t2 t1) rest-eqns)))
       ;; Decomposition + Disagreement
       (t
	(if (or (not (listp t1)) 
		(not (listp t2)) 
		(not (= (list-length t1) (list-length t2))))
	    'failure
	  (unify-aux sub (append (mapcar #'list t1 t2) rest-eqns))))))))


